\begin{tabbing}
$\forall$\=$i$:Id, $k$:Knd, $l$:IdLnk, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$a$:Knd fp$\rightarrow$ Type,\+
\\[0ex]$f$:(${\it tg}$:Id$\times$(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$(${\it da}$(rcv($l$,${\it tg}$))?Void List))) List.
\-\\[0ex]source($l$) $=$ $i$
\\[0ex]$\Rightarrow$ \=@$i$: with declarations \+
\\[0ex]ds:${\it ds}$
\\[0ex]d\=a:${\it da}$\+
\\[0ex]$k$(v) sends $f$ s v on link $l$ 
\-\\[0ex]realizes ${\it es}$.
\\[0ex]($\forall$$x$:Id. vartype($i$;$x$) $\subseteq\rho$ ${\it ds}$($x$)?Top)
\\[0ex]\& ($\forall$$e$:E. loc($e$) $=$ $i$ $\in$ Id $\Rightarrow$ valtype($e$) $\subseteq\rho$ Valtype(${\it da}$;kind($e$)))
\\[0ex]\& ($\forall$$e$:E. isrcv($e$) $\Rightarrow$ lnk($e$) $=$ $l$ $\in$ IdLnk $\Rightarrow$ valtype($e$) $\subseteq\rho$ Valtype(${\it da}$;kind($e$)))
\\[0ex]\& \{$m$:Msg$\mid$ source(mlnk($m$)) $=$ $i$ \} $\subseteq\rho$ Msg($\lambda$$l$,${\it tg}$. ${\it da}$(rcv($l$,${\it tg}$))?Top)
\\[0ex]\& (\=$\forall$$e$:E.\+
\\[0ex]loc($e$) $=$ $i$ $\in$ Id
\\[0ex]$\Rightarrow$ kind($e$) $=$ $k$ $\in$ Knd
\\[0ex]$\Rightarrow$ \=sends($l$;$e$)\+
\\[0ex]$=$
\\[0ex]tagged{-}messages($l$;$\lambda$$z$.$z$ when $e$;val($e$);$f$)
\\[0ex]$\in$ Msg($\lambda$$l$,${\it tg}$. ${\it da}$(rcv($l$,${\it tg}$))?Top) List)
\-\-\-
\end{tabbing}